M:MsgA, l:IdLnk, tg:Id. rcv(l,tg) declared in M  Prop 

latex

Definitions	rcv(l,tg) declared in M, MsgA, Prop, b, x  dom(f), KindDeq, rcv(l,tg), a:A fp B(a), x. t(x), x:A. B(x), Knd, Id, t  T, IdLnk
Lemmas	IdLnk wf, Id wf, Knd wf, fpf-trivial-subtype-top, rcv wf, Kind-deq wf, fpf-dom wf, assert wf, msga wf